Nuprl Lemma : rel_plus-of-restriction
11,40
postcript
pdf
T
:Type,
R
:(
T
T
),
P
:(
T
).
R
|
P
^+ =>
R
^+|
P
latex
Definitions
x
:
A
.
B
(
x
)
,
R1
=>
R2
,
R
^+
,
R
|
P
,
x
:
A
B
(
x
)
,
,
t
T
,
Type
,
P
Q
,
Trans(
T
;
x
,
y
.
E
(
x
;
y
))
,
x
f
y
,
f
(
a
)
,
P
&
Q
,
x
:
A
B
(
x
)
Lemmas
rel
plus
trans
,
restriction-of-transitive
,
rel-rel-plus
,
rel
plus
wf
,
rel-restriction
wf
,
rel
plus
minimal
origin
T:Type, R:(T
T
), P:(T). R|P^+ => R^+|P T:Type, R:(TT), P:(T). R|P^+ => R^+|P x:A. B(x)B(x)
T
Q
B(x)